R:es_realizer{i:l}, P:(ES{i}Prop{i'}).
R-Feasible{i:l}
R-Feasible(R)
 d-realizes{i:l}
 d-realizes([[R]]; es.P(es))
 (es:ES{i}. R-possible{i:l}(R; es)  P(es)) 

latex

Definitions	t  T, f(a), x(s), x:A. B(x), P  Q, D1  D2, D realizes es. P(es), x:AB(x), P & Q, x:A. B(x), A & B, Possible(R;es), Realizer, Type, Prop, ES, x:AB(x), R-Feasible(R), es is an event system of D, {x:A| B(x) }, x. t(x), [[R]]
Lemmas	R-possible wf, d-realizes wf, d-es wf, R-Feasible wf, event system wf, es realizer wf, d-sub-self, R-Dsys wf